package com.googlecode.kipler.reasoning;

import java.util.List;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.ConceptCategory;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.syntax.concept.AtConcept;
import com.googlecode.kipler.syntax.concept.BooleanConcept;
import com.googlecode.kipler.syntax.concept.BooleanConstructor;
import com.googlecode.kipler.syntax.concept.Bottom;
import com.googlecode.kipler.syntax.concept.CardinalityRestriction;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.NaryBooleanConcept;
import com.googlecode.kipler.syntax.concept.Nominal;
import com.googlecode.kipler.syntax.concept.Top;
import com.googlecode.kipler.transformations.CardinalityRestrictionsToABox;
import com.googlecode.kipler.transformations.Transformations;

public class EqualityReasoner {

	private boolean showProof;

	private ProofDialog proofDialog;

	private List<InconsistentLiterals> inconsistenLiterals;

	public EqualityReasoner() {

	}

	public EqualityReasoner(boolean showProof) {
		this.showProof = showProof;
		if (showProof) {
			proofDialog = new ProofDialog();
		}
	}

	public Concept getInterpolant(List<CardinalityRestriction> restrictions,
			List<InconsistentLiterals> literals) {
		CardinalityRestrictionsToABox translator = new CardinalityRestrictionsToABox();
		ABox abox = translator.transform(restrictions);
		Concept result = getInterpolant(abox, literals);
		if (showProof) {
			proofDialog.setVisible(true);
		}
		return result;
	}

	public Concept getInterpolant(ABox abox, List<InconsistentLiterals> literals) {
		inconsistenLiterals = literals;
		return completeTableau(abox);
	}

	private Concept completeTableau(ABox abox) {
		ApplicationResult app = applyLiteralClash(abox);
		if (app.isApplied()) {
			if (showProof) {
				proofDialog.backtrack();
			}
			return app.getInterpolant();
		}
		app = applyNominalClash(abox);
		if (app.isApplied()) {
			if (showProof) {
				proofDialog.backtrack();
			}
			return app.getInterpolant();
		}
		app = applyNominal(abox);
		if (app.isApplied()) {
			if (showProof) {
				proofDialog.backtrack();
			}
			return app.getInterpolant();
		}
		app = applyUnion(abox);
		if (app.isApplied()) {
			if (showProof) {
				proofDialog.backtrack();
			}
			return app.getInterpolant();
		}
		return null;
	}

	private LiteralClashCondition findApplicableLiteralClash(ABox abox) {
		for (Individual i : abox) {
			for (InconsistentLiterals lit : inconsistenLiterals) {
				if (i.getConcepts().containsAll(lit.getLiterals())) {
					return new LiteralClashCondition(i, lit);
				}
			}
		}
		return null;
	}

	private NominalClashCondition findApplicableNominalClash(ABox abox) {
		for (Individual i : abox) {
			for (Concept c : i.getConcepts(ConceptCategory.NOMINAL)) {
				Nominal nom = (Nominal) c;
				Nominal nomNegated = (Nominal) nom.copy().toggleNegated();
				nomNegated.setLeftBiased(true);
				if (i.contains(nomNegated)) {
					Nominal positive = nom.isNegated() ? nomNegated : nom;
					Nominal negative = nom.isNegated() ? nom : nomNegated;
					return new NominalClashCondition(i, positive, negative);
				}
				nomNegated.setLeftBiased(false);
				if (i.contains(nomNegated)) {
					Nominal positive = nom.isNegated() ? nomNegated : nom;
					Nominal negative = nom.isNegated() ? nom : nomNegated;
					return new NominalClashCondition(i, positive, negative);
				}
			}
		}
		return null;
	}

	private ApplicationCondition findApplicableUnion(ABox abox) {
		for (Individual i : abox) {
			for (Concept c : i.getConcepts(ConceptCategory.NARY_UNION)) {
				NaryBooleanConcept union = (NaryBooleanConcept) c;
				boolean noIntersection = true;
				for (Concept op : union.getOperands()) {
					if (i.contains(op)) {
						noIntersection = false;
						break;
					}
				}
				if (noIntersection) {
					return new ApplicationCondition(i, union);
				}
			}
		}
		return null;
	}

	private NominalApplicationCondition findApplicableNominal(ABox abox) {
		for (Individual i : abox) {
			for (Concept c : i.getConcepts(ConceptCategory.NOMINAL)) {
				Nominal nom = (Nominal) c;
				if (!nom.isNegated()) {
					for (Concept d : i.getConcepts()) {
						if (!abox.getIndividual(nom.getName()).contains(d)) {
							return new NominalApplicationCondition(d, i, nom);
						}
					}
				}
			}
		}
		return null;
	}

	private ApplicationResult applyLiteralClash(ABox abox) {
		ApplicationResult result = new ApplicationResult();
		LiteralClashCondition cond = findApplicableLiteralClash(abox);
		if (cond == null) {
			result.setApplied(false);
			return result;
		}
		result.setApplied(true);
		result.setInterpolant(new AtConcept(cond.getIndvidual().getName(), cond
				.getLiterals().getInterpolant()));
		if (showProof) {
			proofDialog.addLiteralClash(cond, result.getInterpolant());
		}
		return result;
	}

	private ApplicationResult applyNominalClash(ABox abox) {
		ApplicationResult result = new ApplicationResult();
		NominalClashCondition cond = findApplicableNominalClash(abox);
		if (cond == null) {
			result.setApplied(false);
			return result;
		}
		result.setApplied(true);
		if (cond.getPositive().isLeftBiased() == cond.getNegative()
				.isLeftBiased()) {
			if (cond.getPositive().isLeftBiased()) {
				result.setInterpolant(new Bottom());
			} else {
				result.setInterpolant(new Top());
			}
		} else {
			Concept c;
			if (cond.getPositive().isLeftBiased()) {
				c = cond.getPositive().copy();

			} else {
				c = cond.getNegative().copy();
			}
			// get rid of bias, might cause problems with equality
			// comparison
			c.setLeftBiased(false);
			result.setInterpolant(new AtConcept(cond.getIndividual().getName(),
					c));
		}
		if (showProof) {
			proofDialog.addNominalClash(cond, result.getInterpolant());
		}
		return result;
	}

	private ApplicationResult applyUnion(ABox abox) {
		ApplicationResult result = new ApplicationResult();
		ApplicationCondition cond = findApplicableUnion(abox);
		if (cond == null) {
			result.setApplied(false);
			return result;
		}
		NaryBooleanConcept union = (NaryBooleanConcept) cond.getConcept();
		NaryBooleanConcept thisInterpolant = new NaryBooleanConcept();
		if (union.isLeftBiased()) {
			thisInterpolant.setConstructor(BooleanConstructor.UNION);
		} else {
			thisInterpolant.setConstructor(BooleanConstructor.INTERSECTION);
		}
		for (Concept op : union.getOperands()) {
			ABox newABox = abox.copy();
			newABox.getIndividual(cond.getIndividual().getName()).add(op);
			if (showProof) {
				proofDialog.branchUnion();
			}
			Concept interpolant = completeTableau(newABox);
			result.setApplied(true);
			if (interpolant == null) {
				result.setInterpolant(null);
				return result;
			} else {
				thisInterpolant.addOperand(interpolant);
			}
		}
		result.setInterpolant(thisInterpolant);
		return result;
	}

	private ApplicationResult applyNominal(ABox abox) {
		ApplicationResult result = new ApplicationResult();
		NominalApplicationCondition cond = findApplicableNominal(abox);
		if (cond == null) {
			result.setApplied(false);
			return result;
		}
		ABox newABox = abox.copy();
		newABox.getIndividual(cond.getT().getName()).add(cond.getPhi());
		if (showProof) {
			proofDialog.branchNominal();
		}
		Concept interpolant = completeTableau(newABox);
		result.setApplied(true);
		if (interpolant == null) {
			result.setInterpolant(null);
		} else {
			Concept newInterpolant = calculateNominalInterpolant(abox, cond,
					interpolant);
			result.setInterpolant(newInterpolant);
		}
		return result;
	}

	private boolean isNominalAppearing(ABox abox, Nominal nom) {
		Individual i = abox.getIndividual(nom.getName());
		for (Concept c : i.getConcepts()) {
			if (c.isLeftBiased() == nom.isLeftBiased()) {
				return true;
			}
		}
		return false;
	}

	private Concept calculateNominalInterpolant(ABox abox,
			NominalApplicationCondition cond, Concept interpolant) {
		Concept result = null;
		if (cond.getT().isLeftBiased() == cond.getPhi().isLeftBiased()) {
			result = interpolant;
		} else if (cond.getT().isLeftBiased() && !cond.getPhi().isLeftBiased()) {
			Nominal rNom = cond.getT().copy();
			rNom.setLeftBiased(false);
			if (isNominalAppearing(abox, rNom)) {
				result = new BooleanConcept(BooleanConstructor.INTERSECTION,
						new AtConcept(cond.getS().getName(), rNom), interpolant);
			} else {
				result = Transformations.replaceNominals(interpolant, cond
						.getS().getName(), cond.getT().getName());
			}
		} else if (!cond.getT().isLeftBiased() && cond.getPhi().isLeftBiased()) {
			Nominal lNom = cond.getT().copy();
			lNom.setLeftBiased(true);
			if (isNominalAppearing(abox, lNom)) {
				lNom.setLeftBiased(false);
				result = new BooleanConcept(BooleanConstructor.UNION,
						new AtConcept(cond.getS().getName(), lNom)
								.toggleNegated(), interpolant);
			} else {
				result = Transformations.replaceNominals(interpolant, cond
						.getS().getName(), cond.getT().getName());
			}
		}
		return result;
	}
}
